\begin{tabbing}
$\forall$$T$:Type, ${\it ll}$:($T$ List List), $n$:\{0..$\parallel$concat(${\it ll}$)$\parallel^{-}$\}.
\\[0ex]$\exists$\=$m$:\{0..$\parallel$${\it ll}$$\parallel^{-}$\}\+
\\[0ex](($\parallel$concat(firstn($m$;${\it ll}$))$\parallel$ $\leq$ $n$)
\\[0ex]c$\wedge$ (($n$ {-} $\parallel$concat(firstn($m$;${\it ll}$))$\parallel$) $<$ $\parallel$${\it ll}$[$m$]$\parallel$)
\\[0ex]c$\wedge$ (concat(${\it ll}$)[$n$] = ${\it ll}$[$m$][($n$ {-} $\parallel$concat(firstn($m$;${\it ll}$))$\parallel$)] $\in$ $T$))
\-
\end{tabbing}